n:, x, y:{0..n}. x before y  upto(n)  (x < y) 

latex

Definitions	{i..j}, t  T, i  j < k, P & Q, A  B, A, P  Q, False, x:A. B(x), ||as||, x:A. B(x), , S  T, suptype(S; T), i  j , t  ...$L, Y, increasing(f;k), if b then t else f fi , tt, ff, l[i], (i = j), SQType(T), {T}, hd(l), nth_tl(n;as), i z j, tl(l), b, i <z j, , , Unit, P  Q, Dec(P), P  Q,
Lemmas	le wf, length upto, select upto, ifthenelse wf, eq int wf, increasing wf, select wf, length wf1, length nil, length cons, non neg length, upto wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, int seg wf, decidable int equal